YES 1.7730000000000001 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule List
  ((intersect :: Eq a => [a ->  [a ->  [a]) :: Eq a => [a ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (\vv2 ->
case vv2 of
  x->  if any (eq x) ys then x : [] else []
  _-> []
) xs


module Maybe where
  import qualified List
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\vv2
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []

is transformed to
intersectBy0 eq ys vv2 = 
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule List
  ((intersect :: Eq a => [a ->  [a ->  [a]) :: Eq a => [a ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 
case vv2 of
  x->  if any (eq x) ys then x : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude



Case Reductions:
The following Case expression
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []

is transformed to
intersectBy00 eq ys x = if any (eq xys then x : [] else []
intersectBy00 eq ys _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule List
  ((intersect :: Eq a => [a ->  [a ->  [a]) :: Eq a => [a ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x  if any (eq x) ys then x : [] else []
intersectBy00 eq ys _ []


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if any (eq xys then x : [] else []

is transformed to
intersectBy000 x True = x : []
intersectBy000 x False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule List
  ((intersect :: Eq a => [a ->  [a ->  [a]) :: Eq a => [a ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys _ []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule List
  ((intersect :: Eq a => [a ->  [a ->  [a]) :: Eq a => [a ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys vw []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ Narrow

mainModule List
  (intersect :: Eq a => [a ->  [a ->  [a])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys vw []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xx2100), Succ(xx401000)) → new_primPlusNat(xx2100, xx401000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xx30100), Succ(xx40100)) → new_primMulNat(xx30100, Succ(xx40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xx3000), Succ(xx4000)) → new_primEqNat(xx3000, xx4000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs2(Just(xx300), Just(xx400), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs1(xx300, xx400, bbb, bbc, bbd)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, app(app(ty_@2, hd), he), fb) → new_esEs3(xx301, xx401, hd, he)
new_esEs0(Left(xx300), Left(xx400), app(ty_[], cc), cd) → new_esEs(xx300, xx400, cc)
new_esEs2(Just(xx300), Just(xx400), app(ty_[], bag)) → new_esEs(xx300, xx400, bag)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, app(app(app(ty_@3, gh), ha), hb), fb) → new_esEs1(xx301, xx401, gh, ha, hb)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), bdb, app(ty_Maybe, bea)) → new_esEs2(xx301, xx401, bea)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), app(ty_[], bbh), bca) → new_esEs(xx300, xx400, bbh)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, fa, app(app(app(ty_@3, baa), bab), bac)) → new_esEs1(xx302, xx402, baa, bab, bac)
new_esEs2(Just(xx300), Just(xx400), app(ty_Maybe, bbe)) → new_esEs2(xx300, xx400, bbe)
new_esEs0(Left(xx300), Left(xx400), app(app(ty_Either, ce), cf), cd) → new_esEs0(xx300, xx400, ce, cf)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), app(app(app(ty_@3, bcd), bce), bcf), bca) → new_esEs1(xx300, xx400, bcd, bce, bcf)
new_esEs(:(xx300, xx301), :(xx400, xx401), app(ty_Maybe, bg)) → new_esEs2(xx300, xx400, bg)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), bdb, app(app(ty_Either, bdd), bde)) → new_esEs0(xx301, xx401, bdd, bde)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), bdb, app(ty_[], bdc)) → new_esEs(xx301, xx401, bdc)
new_esEs0(Right(xx300), Right(xx400), df, app(app(ty_Either, dh), ea)) → new_esEs0(xx300, xx400, dh, ea)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), bdb, app(app(ty_@2, beb), bec)) → new_esEs3(xx301, xx401, beb, bec)
new_esEs0(Left(xx300), Left(xx400), app(ty_Maybe, dc), cd) → new_esEs2(xx300, xx400, dc)
new_esEs0(Right(xx300), Right(xx400), df, app(ty_Maybe, ee)) → new_esEs2(xx300, xx400, ee)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), app(app(app(ty_@3, ff), fg), fh), fa, fb) → new_esEs1(xx300, xx400, ff, fg, fh)
new_esEs(:(xx300, xx301), :(xx400, xx401), app(app(ty_Either, bb), bc)) → new_esEs0(xx300, xx400, bb, bc)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), app(ty_Maybe, bcg), bca) → new_esEs2(xx300, xx400, bcg)
new_esEs(:(xx300, xx301), :(xx400, xx401), cb) → new_esEs(xx301, xx401, cb)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), app(app(ty_Either, fc), fd), fa, fb) → new_esEs0(xx300, xx400, fc, fd)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, app(ty_Maybe, hc), fb) → new_esEs2(xx301, xx401, hc)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), app(app(ty_@2, gb), gc), fa, fb) → new_esEs3(xx300, xx400, gb, gc)
new_esEs(:(xx300, xx301), :(xx400, xx401), app(app(app(ty_@3, bd), be), bf)) → new_esEs1(xx300, xx400, bd, be, bf)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, app(app(ty_Either, gf), gg), fb) → new_esEs0(xx301, xx401, gf, gg)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, fa, app(app(ty_Either, hg), hh)) → new_esEs0(xx302, xx402, hg, hh)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), app(ty_[], eh), fa, fb) → new_esEs(xx300, xx400, eh)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, fa, app(ty_Maybe, bad)) → new_esEs2(xx302, xx402, bad)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), app(app(ty_@2, bch), bda), bca) → new_esEs3(xx300, xx400, bch, bda)
new_esEs0(Right(xx300), Right(xx400), df, app(app(ty_@2, ef), eg)) → new_esEs3(xx300, xx400, ef, eg)
new_esEs0(Right(xx300), Right(xx400), df, app(ty_[], dg)) → new_esEs(xx300, xx400, dg)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), app(ty_Maybe, ga), fa, fb) → new_esEs2(xx300, xx400, ga)
new_esEs(:(xx300, xx301), :(xx400, xx401), app(app(ty_@2, bh), ca)) → new_esEs3(xx300, xx400, bh, ca)
new_esEs2(Just(xx300), Just(xx400), app(app(ty_@2, bbf), bbg)) → new_esEs3(xx300, xx400, bbf, bbg)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), bdb, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(xx301, xx401, bdf, bdg, bdh)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, fa, app(app(ty_@2, bae), baf)) → new_esEs3(xx302, xx402, bae, baf)
new_esEs3(@2(xx300, xx301), @2(xx400, xx401), app(app(ty_Either, bcb), bcc), bca) → new_esEs0(xx300, xx400, bcb, bcc)
new_esEs2(Just(xx300), Just(xx400), app(app(ty_Either, bah), bba)) → new_esEs0(xx300, xx400, bah, bba)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, fa, app(ty_[], hf)) → new_esEs(xx302, xx402, hf)
new_esEs1(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), gd, app(ty_[], ge), fb) → new_esEs(xx301, xx401, ge)
new_esEs0(Left(xx300), Left(xx400), app(app(ty_@2, dd), de), cd) → new_esEs3(xx300, xx400, dd, de)
new_esEs(:(xx300, xx301), :(xx400, xx401), app(ty_[], ba)) → new_esEs(xx300, xx400, ba)
new_esEs0(Left(xx300), Left(xx400), app(app(app(ty_@3, cg), da), db), cd) → new_esEs1(xx300, xx400, cg, da, db)
new_esEs0(Right(xx300), Right(xx400), df, app(app(app(ty_@3, eb), ec), ed)) → new_esEs1(xx300, xx400, eb, ec, ed)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(xx30, :(xx40, xx41), xx5, bb) → new_psPs(xx30, new_esEs4(xx30, xx40, bb), xx41, xx5, bb)
new_psPs(xx11, False, xx13, xx14, ba) → new_psPs0(xx11, xx13, xx14, ba)

The TRS R consists of the following rules:

new_esEs13(Left(xx300), Left(xx400), ty_Ordering, cf) → new_esEs14(xx300, xx400)
new_esEs13(Right(xx300), Right(xx400), eb, app(ty_Maybe, fb)) → new_esEs17(xx300, xx400, fb)
new_esEs15(@3(xx300, xx301, xx302), @3(xx400, xx401, xx402), bae, baf, bag) → new_asAs(new_esEs24(xx300, xx400, bae), new_asAs(new_esEs25(xx301, xx401, baf), new_esEs26(xx302, xx402, bag)))
new_primEqInt(Neg(Succ(xx3000)), Pos(xx400)) → False
new_primEqInt(Pos(Succ(xx3000)), Neg(xx400)) → False
new_esEs8(xx300, xx400, app(app(ty_Either, bf), bg)) → new_esEs13(xx300, xx400, bf, bg)
new_esEs25(xx301, xx401, app(ty_Ratio, bcc)) → new_esEs11(xx301, xx401, bcc)
new_esEs13(Left(xx300), Left(xx400), app(ty_Maybe, dg), cf) → new_esEs17(xx300, xx400, dg)
new_esEs8(xx300, xx400, app(app(app(ty_@3, bh), ca), cb)) → new_esEs15(xx300, xx400, bh, ca, cb)
new_esEs23(xx301, xx401, ty_Integer) → new_esEs18(xx301, xx401)
new_esEs26(xx302, xx402, ty_Float) → new_esEs10(xx302, xx402)
new_esEs24(xx300, xx400, ty_Char) → new_esEs9(xx300, xx400)
new_primEqInt(Neg(Zero), Pos(Succ(xx4000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xx4000))) → False
new_esEs23(xx301, xx401, app(ty_Maybe, bab)) → new_esEs17(xx301, xx401, bab)
new_esEs25(xx301, xx401, app(ty_Maybe, bda)) → new_esEs17(xx301, xx401, bda)
new_esEs24(xx300, xx400, app(ty_Maybe, bbg)) → new_esEs17(xx300, xx400, bbg)
new_esEs13(Left(xx300), Left(xx400), app(app(ty_Either, db), dc), cf) → new_esEs13(xx300, xx400, db, dc)
new_esEs23(xx301, xx401, app(app(ty_Either, he), hf)) → new_esEs13(xx301, xx401, he, hf)
new_esEs24(xx300, xx400, ty_Ordering) → new_esEs14(xx300, xx400)
new_esEs22(xx300, xx400, app(ty_[], ga)) → new_esEs7(xx300, xx400, ga)
new_primMulNat0(Zero, Zero) → Zero
new_esEs17(Just(xx300), Just(xx400), ty_@0) → new_esEs12(xx300, xx400)
new_esEs4(xx30, xx40, ty_Ordering) → new_esEs14(xx30, xx40)
new_esEs4(xx30, xx40, app(ty_[], bc)) → new_esEs7(xx30, xx40, bc)
new_esEs4(xx30, xx40, ty_Integer) → new_esEs18(xx30, xx40)
new_esEs24(xx300, xx400, ty_Integer) → new_esEs18(xx300, xx400)
new_esEs22(xx300, xx400, ty_Ordering) → new_esEs14(xx300, xx400)
new_esEs10(Float(xx300, xx301), Float(xx400, xx401)) → new_esEs6(new_sr(xx300, xx400), new_sr(xx301, xx401))
new_esEs22(xx300, xx400, ty_Char) → new_esEs9(xx300, xx400)
new_esEs4(xx30, xx40, app(ty_Ratio, ff)) → new_esEs11(xx30, xx40, ff)
new_esEs13(Left(xx300), Left(xx400), app(ty_[], cg), cf) → new_esEs7(xx300, xx400, cg)
new_esEs21(xx301, xx401, ty_Int) → new_esEs6(xx301, xx401)
new_esEs25(xx301, xx401, ty_Float) → new_esEs10(xx301, xx401)
new_esEs17(Just(xx300), Just(xx400), ty_Bool) → new_esEs5(xx300, xx400)
new_esEs25(xx301, xx401, ty_Double) → new_esEs16(xx301, xx401)
new_esEs20(xx300, xx400, ty_Int) → new_esEs6(xx300, xx400)
new_sr(Neg(xx3010), Pos(xx4010)) → Neg(new_primMulNat0(xx3010, xx4010))
new_sr(Pos(xx3010), Neg(xx4010)) → Neg(new_primMulNat0(xx3010, xx4010))
new_esEs13(Left(xx300), Left(xx400), ty_@0, cf) → new_esEs12(xx300, xx400)
new_esEs23(xx301, xx401, app(ty_Ratio, hd)) → new_esEs11(xx301, xx401, hd)
new_esEs25(xx301, xx401, app(app(app(ty_@3, bcf), bcg), bch)) → new_esEs15(xx301, xx401, bcf, bcg, bch)
new_esEs24(xx300, xx400, app(app(app(ty_@3, bbd), bbe), bbf)) → new_esEs15(xx300, xx400, bbd, bbe, bbf)
new_esEs8(xx300, xx400, ty_Double) → new_esEs16(xx300, xx400)
new_esEs6(xx30, xx40) → new_primEqInt(xx30, xx40)
new_esEs13(Right(xx300), Right(xx400), eb, ty_@0) → new_esEs12(xx300, xx400)
new_esEs13(Left(xx300), Left(xx400), ty_Char, cf) → new_esEs9(xx300, xx400)
new_esEs13(Left(xx300), Left(xx400), app(app(app(ty_@3, dd), de), df), cf) → new_esEs15(xx300, xx400, dd, de, df)
new_esEs25(xx301, xx401, app(ty_[], bcb)) → new_esEs7(xx301, xx401, bcb)
new_esEs13(Right(xx300), Right(xx400), eb, ty_Integer) → new_esEs18(xx300, xx400)
new_esEs12(@0, @0) → True
new_esEs25(xx301, xx401, ty_Int) → new_esEs6(xx301, xx401)
new_esEs8(xx300, xx400, ty_Int) → new_esEs6(xx300, xx400)
new_esEs7([], [], bc) → True
new_esEs22(xx300, xx400, app(app(ty_Either, gc), gd)) → new_esEs13(xx300, xx400, gc, gd)
new_esEs8(xx300, xx400, ty_Bool) → new_esEs5(xx300, xx400)
new_esEs23(xx301, xx401, app(ty_[], hc)) → new_esEs7(xx301, xx401, hc)
new_esEs4(xx30, xx40, app(ty_Maybe, bef)) → new_esEs17(xx30, xx40, bef)
new_primEqNat0(Zero, Succ(xx4000)) → False
new_primEqNat0(Succ(xx3000), Zero) → False
new_primPlusNat0(Zero, Zero) → Zero
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs13(Left(xx300), Left(xx400), ty_Integer, cf) → new_esEs18(xx300, xx400)
new_esEs17(Just(xx300), Just(xx400), app(ty_[], beg)) → new_esEs7(xx300, xx400, beg)
new_esEs26(xx302, xx402, ty_Ordering) → new_esEs14(xx302, xx402)
new_esEs13(Right(xx300), Right(xx400), eb, ty_Char) → new_esEs9(xx300, xx400)
new_primPlusNat1(Succ(xx210), xx40100) → Succ(Succ(new_primPlusNat0(xx210, xx40100)))
new_esEs23(xx301, xx401, ty_Int) → new_esEs6(xx301, xx401)
new_esEs17(Just(xx300), Just(xx400), ty_Int) → new_esEs6(xx300, xx400)
new_esEs17(Just(xx300), Just(xx400), ty_Float) → new_esEs10(xx300, xx400)
new_esEs7([], :(xx400, xx401), bc) → False
new_esEs7(:(xx300, xx301), [], bc) → False
new_esEs14(EQ, EQ) → True
new_esEs4(xx30, xx40, ty_Char) → new_esEs9(xx30, xx40)
new_esEs14(EQ, LT) → False
new_esEs14(LT, EQ) → False
new_esEs13(Left(xx300), Left(xx400), ty_Float, cf) → new_esEs10(xx300, xx400)
new_esEs4(xx30, xx40, app(app(app(ty_@3, bae), baf), bag)) → new_esEs15(xx30, xx40, bae, baf, bag)
new_esEs26(xx302, xx402, ty_Bool) → new_esEs5(xx302, xx402)
new_esEs13(Right(xx300), Right(xx400), eb, ty_Int) → new_esEs6(xx300, xx400)
new_esEs13(Left(xx300), Left(xx400), ty_Int, cf) → new_esEs6(xx300, xx400)
new_esEs22(xx300, xx400, app(app(ty_@2, ha), hb)) → new_esEs19(xx300, xx400, ha, hb)
new_esEs22(xx300, xx400, ty_@0) → new_esEs12(xx300, xx400)
new_esEs23(xx301, xx401, ty_Bool) → new_esEs5(xx301, xx401)
new_esEs13(Left(xx300), Left(xx400), ty_Bool, cf) → new_esEs5(xx300, xx400)
new_esEs26(xx302, xx402, ty_Int) → new_esEs6(xx302, xx402)
new_esEs26(xx302, xx402, app(ty_[], bdd)) → new_esEs7(xx302, xx402, bdd)
new_esEs25(xx301, xx401, ty_@0) → new_esEs12(xx301, xx401)
new_esEs22(xx300, xx400, app(app(app(ty_@3, ge), gf), gg)) → new_esEs15(xx300, xx400, ge, gf, gg)
new_esEs17(Just(xx300), Just(xx400), ty_Double) → new_esEs16(xx300, xx400)
new_esEs14(GT, EQ) → False
new_esEs14(EQ, GT) → False
new_esEs11(:%(xx300, xx301), :%(xx400, xx401), ff) → new_asAs(new_esEs20(xx300, xx400, ff), new_esEs21(xx301, xx401, ff))
new_sr(Neg(xx3010), Neg(xx4010)) → Pos(new_primMulNat0(xx3010, xx4010))
new_esEs13(Right(xx300), Right(xx400), eb, app(app(ty_@2, fc), fd)) → new_esEs19(xx300, xx400, fc, fd)
new_asAs(False, xx20) → False
new_sr(Pos(xx3010), Pos(xx4010)) → Pos(new_primMulNat0(xx3010, xx4010))
new_primEqNat0(Zero, Zero) → True
new_esEs24(xx300, xx400, ty_Int) → new_esEs6(xx300, xx400)
new_esEs23(xx301, xx401, ty_Ordering) → new_esEs14(xx301, xx401)
new_primMulNat0(Zero, Succ(xx40100)) → Zero
new_primMulNat0(Succ(xx30100), Zero) → Zero
new_esEs22(xx300, xx400, ty_Integer) → new_esEs18(xx300, xx400)
new_esEs17(Just(xx300), Just(xx400), app(app(ty_@2, bfg), bfh)) → new_esEs19(xx300, xx400, bfg, bfh)
new_primMulNat0(Succ(xx30100), Succ(xx40100)) → new_primPlusNat1(new_primMulNat0(xx30100, Succ(xx40100)), xx40100)
new_esEs24(xx300, xx400, ty_Float) → new_esEs10(xx300, xx400)
new_esEs25(xx301, xx401, ty_Bool) → new_esEs5(xx301, xx401)
new_esEs18(Integer(xx300), Integer(xx400)) → new_primEqInt(xx300, xx400)
new_esEs5(False, False) → True
new_esEs25(xx301, xx401, ty_Integer) → new_esEs18(xx301, xx401)
new_esEs5(True, False) → False
new_esEs5(False, True) → False
new_esEs16(Double(xx300, xx301), Double(xx400, xx401)) → new_esEs6(new_sr(xx300, xx400), new_sr(xx301, xx401))
new_esEs26(xx302, xx402, app(ty_Maybe, bec)) → new_esEs17(xx302, xx402, bec)
new_esEs8(xx300, xx400, app(ty_Ratio, be)) → new_esEs11(xx300, xx400, be)
new_esEs4(xx30, xx40, ty_Int) → new_esEs6(xx30, xx40)
new_esEs24(xx300, xx400, ty_Double) → new_esEs16(xx300, xx400)
new_esEs22(xx300, xx400, app(ty_Maybe, gh)) → new_esEs17(xx300, xx400, gh)
new_esEs14(GT, LT) → False
new_esEs14(LT, GT) → False
new_esEs8(xx300, xx400, app(ty_[], bd)) → new_esEs7(xx300, xx400, bd)
new_esEs23(xx301, xx401, ty_Char) → new_esEs9(xx301, xx401)
new_esEs4(xx30, xx40, ty_@0) → new_esEs12(xx30, xx40)
new_esEs14(GT, GT) → True
new_esEs23(xx301, xx401, ty_Double) → new_esEs16(xx301, xx401)
new_esEs8(xx300, xx400, ty_Ordering) → new_esEs14(xx300, xx400)
new_esEs13(Left(xx300), Left(xx400), app(ty_Ratio, da), cf) → new_esEs11(xx300, xx400, da)
new_esEs8(xx300, xx400, ty_Float) → new_esEs10(xx300, xx400)
new_esEs17(Just(xx300), Just(xx400), ty_Integer) → new_esEs18(xx300, xx400)
new_esEs26(xx302, xx402, app(app(ty_@2, bed), bee)) → new_esEs19(xx302, xx402, bed, bee)
new_esEs23(xx301, xx401, ty_@0) → new_esEs12(xx301, xx401)
new_esEs17(Just(xx300), Just(xx400), ty_Ordering) → new_esEs14(xx300, xx400)
new_esEs4(xx30, xx40, ty_Bool) → new_esEs5(xx30, xx40)
new_esEs5(True, True) → True
new_esEs8(xx300, xx400, ty_@0) → new_esEs12(xx300, xx400)
new_primEqInt(Neg(Succ(xx3000)), Neg(Succ(xx4000))) → new_primEqNat0(xx3000, xx4000)
new_esEs24(xx300, xx400, app(ty_Ratio, bba)) → new_esEs11(xx300, xx400, bba)
new_esEs19(@2(xx300, xx301), @2(xx400, xx401), fg, fh) → new_asAs(new_esEs22(xx300, xx400, fg), new_esEs23(xx301, xx401, fh))
new_esEs13(Right(xx300), Left(xx400), eb, cf) → False
new_esEs13(Left(xx300), Right(xx400), eb, cf) → False
new_esEs13(Right(xx300), Right(xx400), eb, app(app(app(ty_@3, eg), eh), fa)) → new_esEs15(xx300, xx400, eg, eh, fa)
new_esEs13(Right(xx300), Right(xx400), eb, app(app(ty_Either, ee), ef)) → new_esEs13(xx300, xx400, ee, ef)
new_esEs22(xx300, xx400, ty_Bool) → new_esEs5(xx300, xx400)
new_esEs17(Just(xx300), Just(xx400), app(app(app(ty_@3, bfc), bfd), bfe)) → new_esEs15(xx300, xx400, bfc, bfd, bfe)
new_esEs17(Just(xx300), Just(xx400), ty_Char) → new_esEs9(xx300, xx400)
new_esEs23(xx301, xx401, app(app(app(ty_@3, hg), hh), baa)) → new_esEs15(xx301, xx401, hg, hh, baa)
new_esEs26(xx302, xx402, app(app(app(ty_@3, bdh), bea), beb)) → new_esEs15(xx302, xx402, bdh, bea, beb)
new_esEs26(xx302, xx402, ty_Integer) → new_esEs18(xx302, xx402)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(xx30, xx40, app(app(ty_Either, eb), cf)) → new_esEs13(xx30, xx40, eb, cf)
new_esEs17(Just(xx300), Just(xx400), app(app(ty_Either, bfa), bfb)) → new_esEs13(xx300, xx400, bfa, bfb)
new_esEs8(xx300, xx400, app(app(ty_@2, cd), ce)) → new_esEs19(xx300, xx400, cd, ce)
new_primEqInt(Neg(Zero), Neg(Succ(xx4000))) → False
new_primEqInt(Neg(Succ(xx3000)), Neg(Zero)) → False
new_esEs17(Nothing, Nothing, bef) → True
new_esEs24(xx300, xx400, app(app(ty_Either, bbb), bbc)) → new_esEs13(xx300, xx400, bbb, bbc)
new_esEs26(xx302, xx402, ty_Char) → new_esEs9(xx302, xx402)
new_esEs22(xx300, xx400, ty_Float) → new_esEs10(xx300, xx400)
new_primPlusNat1(Zero, xx40100) → Succ(xx40100)
new_esEs26(xx302, xx402, app(ty_Ratio, bde)) → new_esEs11(xx302, xx402, bde)
new_esEs22(xx300, xx400, ty_Double) → new_esEs16(xx300, xx400)
new_esEs9(Char(xx300), Char(xx400)) → new_primEqNat0(xx300, xx400)
new_primPlusNat0(Succ(xx2100), Succ(xx401000)) → Succ(Succ(new_primPlusNat0(xx2100, xx401000)))
new_esEs4(xx30, xx40, app(app(ty_@2, fg), fh)) → new_esEs19(xx30, xx40, fg, fh)
new_esEs21(xx301, xx401, ty_Integer) → new_esEs18(xx301, xx401)
new_asAs(True, xx20) → xx20
new_esEs7(:(xx300, xx301), :(xx400, xx401), bc) → new_asAs(new_esEs8(xx300, xx400, bc), new_esEs7(xx301, xx401, bc))
new_esEs23(xx301, xx401, ty_Float) → new_esEs10(xx301, xx401)
new_esEs14(LT, LT) → True
new_esEs25(xx301, xx401, app(app(ty_Either, bcd), bce)) → new_esEs13(xx301, xx401, bcd, bce)
new_esEs13(Left(xx300), Left(xx400), ty_Double, cf) → new_esEs16(xx300, xx400)
new_esEs13(Right(xx300), Right(xx400), eb, ty_Double) → new_esEs16(xx300, xx400)
new_primEqInt(Pos(Succ(xx3000)), Pos(Succ(xx4000))) → new_primEqNat0(xx3000, xx4000)
new_esEs20(xx300, xx400, ty_Integer) → new_esEs18(xx300, xx400)
new_esEs4(xx30, xx40, ty_Float) → new_esEs10(xx30, xx40)
new_esEs13(Left(xx300), Left(xx400), app(app(ty_@2, dh), ea), cf) → new_esEs19(xx300, xx400, dh, ea)
new_esEs17(Just(xx300), Just(xx400), app(ty_Ratio, beh)) → new_esEs11(xx300, xx400, beh)
new_esEs17(Just(xx300), Nothing, bef) → False
new_esEs17(Nothing, Just(xx400), bef) → False
new_esEs26(xx302, xx402, ty_Double) → new_esEs16(xx302, xx402)
new_esEs24(xx300, xx400, app(ty_[], bah)) → new_esEs7(xx300, xx400, bah)
new_esEs25(xx301, xx401, ty_Ordering) → new_esEs14(xx301, xx401)
new_esEs24(xx300, xx400, ty_Bool) → new_esEs5(xx300, xx400)
new_esEs8(xx300, xx400, ty_Integer) → new_esEs18(xx300, xx400)
new_primEqNat0(Succ(xx3000), Succ(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs23(xx301, xx401, app(app(ty_@2, bac), bad)) → new_esEs19(xx301, xx401, bac, bad)
new_esEs26(xx302, xx402, ty_@0) → new_esEs12(xx302, xx402)
new_esEs8(xx300, xx400, ty_Char) → new_esEs9(xx300, xx400)
new_esEs25(xx301, xx401, app(app(ty_@2, bdb), bdc)) → new_esEs19(xx301, xx401, bdb, bdc)
new_esEs22(xx300, xx400, ty_Int) → new_esEs6(xx300, xx400)
new_esEs17(Just(xx300), Just(xx400), app(ty_Maybe, bff)) → new_esEs17(xx300, xx400, bff)
new_esEs13(Right(xx300), Right(xx400), eb, app(ty_Ratio, ed)) → new_esEs11(xx300, xx400, ed)
new_esEs13(Right(xx300), Right(xx400), eb, app(ty_[], ec)) → new_esEs7(xx300, xx400, ec)
new_esEs13(Right(xx300), Right(xx400), eb, ty_Ordering) → new_esEs14(xx300, xx400)
new_esEs4(xx30, xx40, ty_Double) → new_esEs16(xx30, xx40)
new_esEs25(xx301, xx401, ty_Char) → new_esEs9(xx301, xx401)
new_primEqInt(Pos(Zero), Pos(Succ(xx4000))) → False
new_esEs22(xx300, xx400, app(ty_Ratio, gb)) → new_esEs11(xx300, xx400, gb)
new_primEqInt(Pos(Succ(xx3000)), Pos(Zero)) → False
new_esEs13(Right(xx300), Right(xx400), eb, ty_Float) → new_esEs10(xx300, xx400)
new_esEs24(xx300, xx400, app(app(ty_@2, bbh), bca)) → new_esEs19(xx300, xx400, bbh, bca)
new_esEs24(xx300, xx400, ty_@0) → new_esEs12(xx300, xx400)
new_esEs26(xx302, xx402, app(app(ty_Either, bdf), bdg)) → new_esEs13(xx302, xx402, bdf, bdg)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primPlusNat0(Succ(xx2100), Zero) → Succ(xx2100)
new_primPlusNat0(Zero, Succ(xx401000)) → Succ(xx401000)
new_esEs13(Right(xx300), Right(xx400), eb, ty_Bool) → new_esEs5(xx300, xx400)
new_esEs8(xx300, xx400, app(ty_Maybe, cc)) → new_esEs17(xx300, xx400, cc)

The set Q consists of the following terms:

new_esEs22(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs14(GT, EQ)
new_esEs14(EQ, GT)
new_esEs24(x0, x1, ty_Double)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primPlusNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_primPlusNat1(Zero, x0)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs8(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Int)
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs8(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs17(Just(x0), Nothing, x1)
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7([], :(x0, x1), x2)
new_esEs23(x0, x1, ty_Bool)
new_esEs4(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs13(Left(x0), Right(x1), x2, x3)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs22(x0, x1, ty_@0)
new_esEs8(x0, x1, ty_Char)
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(x0, x1)
new_esEs26(x0, x1, ty_@0)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(False, True)
new_esEs5(True, False)
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_asAs(False, x0)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs11(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs14(LT, GT)
new_esEs14(GT, LT)
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Char(x0), Char(x1))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Char)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs5(True, True)
new_esEs19(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs15(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqNat0(Zero, Zero)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs4(x0, x1, ty_@0)
new_primMulNat0(Zero, Succ(x0))
new_esEs5(False, False)
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_sr(Pos(x0), Pos(x1))
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(x0, x1, ty_Bool)
new_esEs12(@0, @0)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs7([], [], x0)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs20(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Double(x0, x1), Double(x2, x3))
new_esEs24(x0, x1, ty_Char)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primPlusNat1(Succ(x0), x1)
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs22(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs18(Integer(x0), Integer(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Double)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs8(x0, x1, ty_Float)
new_esEs10(Float(x0, x1), Float(x2, x3))
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, ty_Double)
new_esEs14(EQ, LT)
new_esEs14(LT, EQ)
new_esEs23(x0, x1, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_sr(Neg(x0), Neg(x1))
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_primPlusNat0(Succ(x0), Zero)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs26(x0, x1, ty_Double)
new_esEs14(GT, GT)
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs24(x0, x1, ty_Int)
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_esEs4(x0, x1, ty_Integer)
new_esEs8(x0, x1, ty_Ordering)
new_esEs8(x0, x1, ty_@0)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_@0)
new_esEs14(EQ, EQ)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_primPlusNat0(Zero, Zero)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs7(:(x0, x1), [], x2)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs14(LT, LT)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs17(Nothing, Nothing, x0)
new_esEs23(x0, x1, ty_Char)
new_esEs17(Nothing, Just(x0), x1)
new_esEs7(:(x0, x1), :(x2, x3), x4)
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Zero, Succ(x0))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Float)
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_asAs(True, x0)
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs20(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primMulNat0(Succ(x0), Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(xx4, :(xx30, xx31), ba) → new_foldr(xx4, xx31, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: